Contained herein is material that is subject to copyright protection. The copyright owner has no objection to the facsimile reproduction of the patent disclosure by any person as it appears in the Patent and Trademark Office patent files or records, but otherwise reserves all rights to the copyright whatsoever.
1. Field of the Invention
The invention relates generally to the field of design verification. More particularly, the invention relates to a method of automatically formulating design verification checks based upon design intent.
2. Description of the Related Art
The objective of design verification is to ensure that errors are absent from a design. Deep sub-micron integrated circuit (IC) manufacturing technology is enabling IC designers to put millions of transistors on a single IC. Following Moore""s law, design complexity is doubling every 12-18 months, which causes design verification complexity to increase at an exponential rate. In addition, competitive pressures are putting increased demands on reducing time to market. The combination of these forces has caused an ever worsening xe2x80x9cverification crisisxe2x80x9d.
Today""s design flow starts with a specification for the design. The designer then implements the design in a language model, typically Hardware Description Language (HDL). This model is typically verified to discover incorrect input/output (I/O) behavior via a stimulus in expected results out paradigm at the top level of the design.
By far the most popular method of functional verification today, simulation-based functional verification, is widely used within the digital design industry as a method for finding defects within designs. A very wide variety of products are available in the market to support simulation-based verification methodologies. However, a fundamental problem with conventional simulation-based verification approaches is that they are vector and testbench limited.
Simulation-based verification is driven by a testbench that explicitly generates the vectors to achieve stimulus coverage and also implements the checking mechanism. Testbenches create a fundamental bottleneck in simulation-based functional verification. In order to verify a design hierarchy level, a testbench must be generated for it. This creates verification overhead for coding and debugging the testbench. Hence, a significant amount of expensive design and verification engineering resources are needed to produce results in a cumbersome and slow process.
Several methods have been attempted by Electronic Design Automation (EDA) companies today in order to address the shortcomings of simulation. However, none of these attempts address this fundamental limitation of the process. For example, simulation vendors have tried to meet the simulation throughput challenge by increasing the performance of hardware and software simulators thereby allowing designers to process a greater number of vectors in the same amount of simulation time. While this does increase stimulus coverage, the results are incremental. The technology is not keeping pace with the required growth rate and the verification processes are lagging in achieving the required stimulus coverage.
Formal verification is another class of tools that has entered the functional verification arena. These tools rely on mathematical analysis rather than simulation of the design. The strong selling point of formal verification is the fact that the results hold true for all possible input combinations to the design. However, in practice this high level of stimulus coverage has come at the cost of both error coverage and particularly usability. While some formal techniques are available, they are not widely used because they typically require the designer to know the details of how the tool works in order to operate it. Formal verification tools generally fall into two classes: (1) equivalence checking, and (2) model checking.
Equivalence checking is a form of formal verification that provides designers with the ability to perform RTL-to-gate and gate-to-gate comparisons of a design to determine if they are functionally equivalent. Importantly, however, equivalence checking is not a method of functional verification. Rather, equivalence checking merely provides an alternate solution for comparing a design representation to an original golden reference. It does not verify the functionality of the original golden reference for the design. Consequently, the original golden reference must be functionally verified using other methods.
Model checking is a functional verification technology that requires designers to formulate properties about the design""s expected behavior. Each property is then checked against an exhaustive set of functional behaviors in the design. The limitation of this approach is that the designer is responsible for exactly specifying the set of properties to be verified. The property specification languages are new and obscure. Usually the technology runs into capacity problems and the designer has to engage with the tools to solve the problems. There are severe limits on the size of the design and the scope of problems that can be analyzed. For example, the designer does not know which properties are necessary for complete analysis of the design. Further, specifying a large number of properties does not correlate well with better error coverage. Consequently, model checking has proven to be very difficult to use and has not provided much value in the verification process.
In view of the foregoing it would be desirable to create a verification methodology to create high quality designs without the need for simulation testbench and to increase the productiveness of design engineers by minimizing the tool setup effort and report processing effort. In particular, it would be advantageous to abstract the internal details of the tools from the user to make these tools more accessible to designers. For example, it would be advantageous to allow a verification methodology to be employed while allowing the designer to think about characteristics of the design. In this manner, the designer can think in terms of time progression of data at various design elements (entities) rather than the implementation of the verification tool. Additionally, rather than requiring the designer to write properties in a complex and arcane language, it would be advantageous to automatically formulate a list of verification checks that, if satisfied, would guarantee the absence of errors in a design with a high level of confidence. Finally, it would be advantageous to maintain and utilize relationships among the list of automatically generated verification checks to facilitate error reporting and to prune the error space for more efficient run-time processing.
A method and apparatus are described that facilitate analysis of the intended flow of logical signals between key points in a design. According to one aspect of the present invention, hardware design defects can be detected using a novel Intent-Driven Verification process. First, a representation of a hardware design and information regarding the intended flow of logical signals among variables in the representation are received. Then, the existence of potential errors in the hardware design may be inferred based upon the information regarding the intended flow of logical signals by (1) translating the information regarding the intended flow of logical signals into a comprehensive set of checks that must hold true in order for the hardware design to operate in accordance with the intended flow of logical signals, and (2) determining if any of the checks can be violated during operation of circuitry represented by the hardware design. Advantageously, in this manner, the designer is not required to manually code individual monitors for each property he/she would like to verify. Rather, verification cycle time and resource requirements are reduced by allowing the designer to simply annotate a language representation of the hardware design under test with information regarding the desired/expected interaction between components of the design and/or the designer""s expectations for acceptable functional behavior (in terms of the expected state of variables at various points in the control flow structure of a finite state machine associated with the hardware design representation, for example) and the generation of a comprehensive set of checks for identifying the intent gap is automatically performed.
According to another aspect of the present invention, a method is provided for explicitly associating state information with variables of a language description of a hardware design. Information regarding the intended flow of logical signals among the variables, which represent interconnects in the hardware design through with the logical signals pass, is received. Then, the intended flow of logical signals is modeled by associating state information with the variables in accordance with the intended flow of logical signals. Advantageously, in this manner, the integrity of the data flow can be verified by confirming checks that are expressed as a function of the states associated with the variables.
According to another aspect of the present invention, a comprehensive set of design verification checks may be formulated by applying predetermined properties to an annotated hardware design representation. Information regarding the intended flow of logical signals in the hardware design is received by way of annotations in a control file or annotations embedded in the hardware design representation itself. The annotations include (1) an indication of one or more variables in the representation of the hardware design through which the logical signals pass, and (2) an indication of one or more conditions under which each of the one or more variables are to be associated with each of a set of states. Checks are then automatically formulated based upon a predetermined set of properties that must hold true in order for the hardware design to operate in accordance with the intended flow. Each of the checks is capable of evaluation with reference to the states associated with the one or more variables during propagation of the logical signals.
According to yet another aspect of the present invention, multiple design verification checks associated with a hardware design are linked by determining dependency relationships among the multiple design verification checks. Each of the design verification checks represent a condition that must hold true in order for the hardware design to operate in accordance with an intended flow of logical signals in the hardware design.
Other features of the present invention will be apparent from the accompanying drawings and from the detailed description that follows.